$\forall$$T$:Type, ${\it as}$, ${\it bs}$:$T$ List. rev(${\it as}$ @ ${\it bs}$) $=$ (rev(${\it bs}$) @ rev(${\it as}$)) $\in$ $T$ List